Inference at * 1 
Iof proof for Lemma comp nat ind a:



1. P : {k}
2. i:. (j:. (j < i)  P(j))  P(i)
3. i : 
  P(i) 

latex

 by ((% Generalize % 
Assert j,s:. (s < j)  P(s)) 
ACollapseTHEN (IfLabL 
AC[`assertion`,Id 

AC[`;`main`,((InstHyp [i + 1;i] (-1)) 
ACollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
AC),(first_nat 3:n)) (first_tok :t) inil_term)))])) 

latex

AC1: .....assertion..... NILNIL

AC1:   j,s:. (s < j)  P(s)
AC.

Definitions	False, A, A  B, t  T, P  Q, , x:A. B(x),
Lemmas	le wf